1. Field of the Invention
The present invention relates in general to verifying designs and in particular to verifying a logic function in a netlist. Still more particularly, the present invention relates to a system, method and computer program product for performing heuristic constraint simplification.
2. Description of the Related Art
With the increasing penetration of microprocessor-based systems into every facet of human activity, demands have increased on the microprocessor development and production community to produce systems that are free from data corruption. Microprocessors have become involved in the performance of a vast array of critical functions, and the involvement of microprocessors in the important tasks of daily life has heightened the expectation of reliability of calculative results. Whether the impact of errors would be measured in human lives or in mere dollars and cents, consumers of microprocessors have lost tolerance for error-prone results. Consumers will not tolerate, by way of example, miscalculations on the floor of the stock exchange, in the medical devices that support human life, or in the computers that control their automobiles. All of these activities represent areas where the need for reliable microprocessor results has risen to a mission-critical concern.
Formal verification techniques, semiformal verification techniques and simulation provide powerful tools for discovering errors and verifying the correctness of logic designs. Formal verification techniques, semiformal verification techniques and simulation frequently expose probabilistically uncommon scenarios that may result in a functional design failure. Additionally, formal verification techniques provide the opportunity to prove that a design is correct (e.g., that no failing scenario exists).
One commonly-used approach to formal, semiformal, and simulation analysis for applications operating on representations of circuit structures is to represent the underlying logical problem structurally (as a circuit graph), and to perform explicit or symbolic evaluation of that circuit graph.
In such an approach, a logical problem is represented structurally. Explicit simulation-based approaches to hardware verification are scalable to very large designs, though suffer from the coverage problem that generally limits them to yielding exponentially decreasing coverage with respect to design size. Formal verification techniques overcome the coverage problem of simulation, yielding exhaustive coverage, though suffer from computational complexity that limits their application to smaller designs.
Formal verification techniques generally require exponential resources with respect to the number of state elements and inputs of a design under verification. Various techniques have been proposed to address the reduction in the number of state elements. Constraints are often used in verification to prune the possible input stimulus in certain states of the design. For example, a constraint may state “if the design's buffer is full, then constrain the input stimulus to prevent new transfers into the design”. Semantically, the verification tool will typically discard any states for which a constraint evaluates to a 0 (i.e., the verification tool may never produce a failing scenario showing a violation of some property of the design, if that scenario does not adhere to all the constraints for all time-steps prior to the failure). In this previous example, it would be illegal for the verification tool to produce a trace of length “i” showing a violation of some property, if that trace illustrated the scenario that the buffer was full and a new transfer was initiated into the design between time 0 and i (inclusive).
The modeling of design environments using constraints has gained widespread industrial application, and most verification languages include constructs for specifying constraints. It is therefore critical for verification tools to intelligently leverage constraints to enhance the overall verification process. Though constraints enable efficient modeling of design environments, they pose several challenges to transformation and verification algorithms. For example, transformation methods like retiming may be required to generate even a sub-optimal result in the presence of constraints. Redundancy removal methods are also restricted in their ability to simplify the cones of the constraints.
Constraints also pose challenges to testcase generation and explicit state analysis. Though constraint-preserving testcase generation for simulation has been widely researched, the prior art does not effectively solve the problem of the preservation of “dead-end constraints”, which entail states for which there is no legal stimulus. Dead-end constraints tend to reduce the efficiency of explicit-state analysis, as well as semi-formal search; when a dead-end state is reached, the only recourse is to backtrack to an earlier state. No prior work has adequately addressed the simplification of dead-end constraints.
What is needed is an improved method for heuristic constraint simplification.